p(0(x1)) → 0(s(s(p(x1))))
p(s(x1)) → x1
p(p(s(x1))) → p(x1)
f(s(x1)) → g(s(x1))
g(x1) → i(s(half(x1)))
i(x1) → f(p(x1))
half(0(x1)) → 0(s(s(half(x1))))
half(s(s(x1))) → s(half(p(p(s(s(x1))))))
0(x1) → x1
rd(0(x1)) → 0(0(0(0(0(0(rd(x1)))))))
↳ QTRS
↳ DependencyPairsProof
p(0(x1)) → 0(s(s(p(x1))))
p(s(x1)) → x1
p(p(s(x1))) → p(x1)
f(s(x1)) → g(s(x1))
g(x1) → i(s(half(x1)))
i(x1) → f(p(x1))
half(0(x1)) → 0(s(s(half(x1))))
half(s(s(x1))) → s(half(p(p(s(s(x1))))))
0(x1) → x1
rd(0(x1)) → 0(0(0(0(0(0(rd(x1)))))))
F(s(x1)) → G(s(x1))
G(x1) → HALF(x1)
HALF(s(s(x1))) → P(p(s(s(x1))))
HALF(s(s(x1))) → P(s(s(x1)))
P(p(s(x1))) → P(x1)
HALF(0(x1)) → 01(s(s(half(x1))))
RD(0(x1)) → RD(x1)
RD(0(x1)) → 01(0(0(rd(x1))))
P(0(x1)) → P(x1)
HALF(0(x1)) → HALF(x1)
RD(0(x1)) → 01(0(0(0(0(rd(x1))))))
P(0(x1)) → 01(s(s(p(x1))))
RD(0(x1)) → 01(0(rd(x1)))
HALF(s(s(x1))) → HALF(p(p(s(s(x1)))))
G(x1) → I(s(half(x1)))
I(x1) → P(x1)
RD(0(x1)) → 01(rd(x1))
RD(0(x1)) → 01(0(0(0(0(0(rd(x1)))))))
I(x1) → F(p(x1))
RD(0(x1)) → 01(0(0(0(rd(x1)))))
p(0(x1)) → 0(s(s(p(x1))))
p(s(x1)) → x1
p(p(s(x1))) → p(x1)
f(s(x1)) → g(s(x1))
g(x1) → i(s(half(x1)))
i(x1) → f(p(x1))
half(0(x1)) → 0(s(s(half(x1))))
half(s(s(x1))) → s(half(p(p(s(s(x1))))))
0(x1) → x1
rd(0(x1)) → 0(0(0(0(0(0(rd(x1)))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
F(s(x1)) → G(s(x1))
G(x1) → HALF(x1)
HALF(s(s(x1))) → P(p(s(s(x1))))
HALF(s(s(x1))) → P(s(s(x1)))
P(p(s(x1))) → P(x1)
HALF(0(x1)) → 01(s(s(half(x1))))
RD(0(x1)) → RD(x1)
RD(0(x1)) → 01(0(0(rd(x1))))
P(0(x1)) → P(x1)
HALF(0(x1)) → HALF(x1)
RD(0(x1)) → 01(0(0(0(0(rd(x1))))))
P(0(x1)) → 01(s(s(p(x1))))
RD(0(x1)) → 01(0(rd(x1)))
HALF(s(s(x1))) → HALF(p(p(s(s(x1)))))
G(x1) → I(s(half(x1)))
I(x1) → P(x1)
RD(0(x1)) → 01(rd(x1))
RD(0(x1)) → 01(0(0(0(0(0(rd(x1)))))))
I(x1) → F(p(x1))
RD(0(x1)) → 01(0(0(0(rd(x1)))))
p(0(x1)) → 0(s(s(p(x1))))
p(s(x1)) → x1
p(p(s(x1))) → p(x1)
f(s(x1)) → g(s(x1))
g(x1) → i(s(half(x1)))
i(x1) → f(p(x1))
half(0(x1)) → 0(s(s(half(x1))))
half(s(s(x1))) → s(half(p(p(s(s(x1))))))
0(x1) → x1
rd(0(x1)) → 0(0(0(0(0(0(rd(x1)))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
RD(0(x1)) → RD(x1)
p(0(x1)) → 0(s(s(p(x1))))
p(s(x1)) → x1
p(p(s(x1))) → p(x1)
f(s(x1)) → g(s(x1))
g(x1) → i(s(half(x1)))
i(x1) → f(p(x1))
half(0(x1)) → 0(s(s(half(x1))))
half(s(s(x1))) → s(half(p(p(s(s(x1))))))
0(x1) → x1
rd(0(x1)) → 0(0(0(0(0(0(rd(x1)))))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
RD(0(x1)) → RD(x1)
The value of delta used in the strict ordering is 1/16.
POL(RD(x1)) = (1/4)x_1
POL(0(x1)) = 1/4 + (2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
p(0(x1)) → 0(s(s(p(x1))))
p(s(x1)) → x1
p(p(s(x1))) → p(x1)
f(s(x1)) → g(s(x1))
g(x1) → i(s(half(x1)))
i(x1) → f(p(x1))
half(0(x1)) → 0(s(s(half(x1))))
half(s(s(x1))) → s(half(p(p(s(s(x1))))))
0(x1) → x1
rd(0(x1)) → 0(0(0(0(0(0(rd(x1)))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
P(p(s(x1))) → P(x1)
P(0(x1)) → P(x1)
p(0(x1)) → 0(s(s(p(x1))))
p(s(x1)) → x1
p(p(s(x1))) → p(x1)
f(s(x1)) → g(s(x1))
g(x1) → i(s(half(x1)))
i(x1) → f(p(x1))
half(0(x1)) → 0(s(s(half(x1))))
half(s(s(x1))) → s(half(p(p(s(s(x1))))))
0(x1) → x1
rd(0(x1)) → 0(0(0(0(0(0(rd(x1)))))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
P(p(s(x1))) → P(x1)
P(0(x1)) → P(x1)
The value of delta used in the strict ordering is 1/2.
POL(P(x1)) = (2)x_1
POL(p(x1)) = 2 + (1/2)x_1
POL(s(x1)) = (4)x_1
POL(0(x1)) = 1/4 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
p(0(x1)) → 0(s(s(p(x1))))
p(s(x1)) → x1
p(p(s(x1))) → p(x1)
f(s(x1)) → g(s(x1))
g(x1) → i(s(half(x1)))
i(x1) → f(p(x1))
half(0(x1)) → 0(s(s(half(x1))))
half(s(s(x1))) → s(half(p(p(s(s(x1))))))
0(x1) → x1
rd(0(x1)) → 0(0(0(0(0(0(rd(x1)))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
HALF(0(x1)) → HALF(x1)
HALF(s(s(x1))) → HALF(p(p(s(s(x1)))))
p(0(x1)) → 0(s(s(p(x1))))
p(s(x1)) → x1
p(p(s(x1))) → p(x1)
f(s(x1)) → g(s(x1))
g(x1) → i(s(half(x1)))
i(x1) → f(p(x1))
half(0(x1)) → 0(s(s(half(x1))))
half(s(s(x1))) → s(half(p(p(s(s(x1))))))
0(x1) → x1
rd(0(x1)) → 0(0(0(0(0(0(rd(x1)))))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
HALF(0(x1)) → HALF(x1)
Used ordering: Polynomial interpretation [25,35]:
HALF(s(s(x1))) → HALF(p(p(s(s(x1)))))
The value of delta used in the strict ordering is 1/2.
POL(HALF(x1)) = (1/4)x_1
POL(s(x1)) = x_1
POL(p(x1)) = x_1
POL(0(x1)) = 2 + x_1
p(0(x1)) → 0(s(s(p(x1))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
0(x1) → x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
HALF(s(s(x1))) → HALF(p(p(s(s(x1)))))
p(0(x1)) → 0(s(s(p(x1))))
p(s(x1)) → x1
p(p(s(x1))) → p(x1)
f(s(x1)) → g(s(x1))
g(x1) → i(s(half(x1)))
i(x1) → f(p(x1))
half(0(x1)) → 0(s(s(half(x1))))
half(s(s(x1))) → s(half(p(p(s(s(x1))))))
0(x1) → x1
rd(0(x1)) → 0(0(0(0(0(0(rd(x1)))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
F(s(x1)) → G(s(x1))
I(x1) → F(p(x1))
G(x1) → I(s(half(x1)))
p(0(x1)) → 0(s(s(p(x1))))
p(s(x1)) → x1
p(p(s(x1))) → p(x1)
f(s(x1)) → g(s(x1))
g(x1) → i(s(half(x1)))
i(x1) → f(p(x1))
half(0(x1)) → 0(s(s(half(x1))))
half(s(s(x1))) → s(half(p(p(s(s(x1))))))
0(x1) → x1
rd(0(x1)) → 0(0(0(0(0(0(rd(x1)))))))